st-lookup(tab;x)
== let K,p,f = tab in 
== let n = mu(n.p<n  Kn  1of(f(n)) =a1 x) in 
== if p<n  Kn inr() else inl(2of(f(n))) fi 

latex

---

clarification:

st-lookup(tab;x)
== let K,p,f = tab in 
== let n = mu(n.p<n  Kn  eq_atom1(1of(f(n));x)) in 
== if p<n  Kn inr() else inl(2of(f(n))) fi 

latex

Definitions	let x,y,z = a in t(x;y;z), let x = a in b(x), mu(f), x.A(x), eq_atom$n(x;y), 1of(t), if b t else f fi, p  q, i<j, ij, inr(x), , inl(x), 2of(t), f(a)
FDL editor aliases	st-lookup